ePMC

Benchmark
Model:wlan v.1 (MDP)
Parameter(s)MAX_BACKOFF = 4, COL = 0
Property:sent (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files wlan.4.prism --model-input-type prism --property-input-files wlan.props --property-input-names sent --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const COL=0
Execution
Walltime:21.65116286277771s
Return code:0
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property sent
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 15912 15912
build-model-states-explored 35492 19580
build-model-states-explored 53391 17899
build-model-states-explored 72679 19288
build-model-states-explored 93716 21037
build-model-states-explored 117058 23342
build-model-states-explored 137965 20907
build-model-states-explored 160881 22916
build-model-states-explored 183807 22926
build-model-states-explored 206652 22845
build-model-states-explored 229708 23056
build-model-states-explored 254261 24553
build-model-states-explored 278804 24543
build-model-states-explored 303451 24647
build-model-states-explored 328136 24685
build-model-done 345000 15
iterating
iterating-progress-unbounded 385 1.0 1
iterating-progress-unbounded 781 0.010160377369844376 2
iterating-progress-unbounded 1177 2.2318245499794063E-5 3
iterating-progress-unbounded 1573 8.196119528855924E-7 4
iterating-done 1591 4
model-checking-done 21
command-check-result-is true sent